Nuprl Lemma : wellfounded-anti-reflexive
0,22
postcript
pdf
T
:Type,
R
:(
T
T
Prop). WellFnd{i}(
T
;
x
,
y
.
R
(
x
,
y
))
(
a
:
T
.
R
(
a
,
a
))
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
x
.
t
(
x
)
,
{
T
}
,
False
,
P
Q
,
Prop
,
A
,
x
:
A
.
B
(
x
)
,
t
T
,
x
(
s1
,
s2
)
Lemmas
not
wf
,
wellfounded
wf
origin
T:Type, R:(T
TProp). WellFnd{i}(T;x,y.R(x,y)) 
(a:T. 
R(a,a)) T:Type, R:(TTProp). WellFnd{i}(T;x,y.R(x,y)) (a:T. R(a,a)) 
x,y. t(x;y)x. t(x) QAx:A. B(x)
T